Nuprl Lemma : es-msgs_wf
0,22
postcript
pdf
the_es
:ES,
l
:IdLnk,
e'
:E. msgs(
l
;before(
e'
))
(Msg on
l
) List
latex
Definitions
E
,
b
,
haslnk(
l
;
e
)
,
rcvs(
l
;before(
e'
))
,
IdLnk
,
ES
,
msgs(
l
;before(
e'
))
,
P
Q
,
map(
f
;
as
)
,
(Msg on
l
)
,
emsg(
e
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
es-msg
wf2
,
es-Msgl
wf
,
map
wf
,
es-haslnk
wf
,
assert
wf
,
es-rcvs
wf
,
event
system
wf
,
IdLnk
wf
,
es-E
wf
origin
the_es:ES, l:IdLnk, e':E. msgs(l;before(e')) 
(Msg on l) List the_es:ES, l:IdLnk, e':E. msgs(l;before(e')) (Msg on l) List 
b
Qx:A. B(x) T